| 1: | a__f(X) | → a__if(mark(X),c,f(true)) | |
| 2: | a__if(true,X,Y) | → mark(X) | |
| 3: | a__if(false,X,Y) | → mark(Y) | |
| 4: | mark(f(X)) | → a__f(mark(X)) | |
| 5: | mark(if(X1,X2,X3)) | → a__if(mark(X1),mark(X2),X3) | |
| 6: | mark(c) | → c | |
| 7: | mark(true) | → true | |
| 8: | mark(false) | → false | |
| 9: | a__f(X) | → f(X) | |
| 10: | a__if(X1,X2,X3) | → if(X1,X2,X3) | |
| 11: | A__F(X) | → A__IF(mark(X),c,f(true)) | |
| 12: | A__F(X) | → MARK(X) | |
| 13: | A__IF(true,X,Y) | → MARK(X) | |
| 14: | A__IF(false,X,Y) | → MARK(Y) | |
| 15: | MARK(f(X)) | → A__F(mark(X)) | |
| 16: | MARK(f(X)) | → MARK(X) | |
| 17: | MARK(if(X1,X2,X3)) | → A__IF(mark(X1),mark(X2),X3) | |
| 18: | MARK(if(X1,X2,X3)) | → MARK(X1) | |
| 19: | MARK(if(X1,X2,X3)) | → MARK(X2) | |